$\forall$$A$, $B$:Realizer.
\\[0ex]Rplus?($A$)
\\[0ex]$\Rightarrow$ ($\forall$$i$:Id. R{-}da(Rplus{-}left($A$);$i$) $\parallel$ R{-}da(Rplus{-}right($A$);$i$))
\\[0ex]$\Rightarrow$ (R{-}interface($A$;$B$) $\Leftrightarrow$ R{-}interface(Rplus{-}left($A$);$B$) \& R{-}interface(Rplus{-}right($A$);$B$))